/*
 *  SableJBDD, a Java Binary Decision Diagram package.
 *  Copyright (C) 2003  Feng Qian
 *
 *  This library is free software; you can redistribute it and/or
 *  modify it under the terms of the GNU Lesser General Public
 *  License as published by the Free Software Foundation; either
 *  version 2.1 of the License, or (at your option) any later version.
 *
 *  This library is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 *  Lesser General Public License for more details.
 *
 *  You should have received a copy of the GNU Lesser General Public
 *  License along with this library; if not, write to the Free Software
 *  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
//$Id: PhantomUniqueTable.java,v 1.3 2004/03/15 02:07:07 fqian Exp $
package SableJBDD.bdd.internal;

import SableJBDD.bdd.*;
import SableJBDD.cache.CacheProfiler;
import SableJBDD.bdd.util.HashFunction;
import java.lang.ref.*;
import java.lang.reflect.*;

/**
 * A phantom unique table implements UniqueTable interface, and can recycle 
 * nodes not reachable from other programs other than this unique table.
 * <p>
 * Implementation details:
 * <ul>
 * <li>A free node pool preallocates a set of nodes (can be dynamically expended),
 * and free nodes are strongly reachable to prevent them from being collected.
 * <li>When the unique table makes a new node, it acquires a free node from
 * the free node pool, and also puts it in the unique table indirectly via a phantom
 * reference. The reference is registered with a reference queue.
 * <li>After each garbage collection, GC puts phantom referencs that are not
 * strongly reachable into the reference queue. When there are not enough free nodes, 
 * the pool can remove phantom references from the queue and put them back to
 * the pool.
 * <li>If after a collection, the free nodes ratio is below a pre-defined
 * threshold, it expends the node pool by allocating more nodes from heaps.
 * </ul>
 *
 * @author Feng Qian
 */
public class PhantomUniqueTable extends CacheProfiler implements UniqueTable{
  
  private PhantomJBddNodePool nodePool;

  private PhantomJBddNodeReference[] tableEntries;
  private int tableSize;
  public PhantomUniqueTable(int inittablesize, int initpoolsize) {
    this.tableEntries = new PhantomJBddNodeReference[inittablesize];
    this.tableSize = inittablesize;
    this.nodePool = new PhantomJBddNodePool(this, initpoolsize, .25f, .75f);
  }
  
  /**
   * Finds or creates a BddNode by a triple key.
   * @param var the BDD variable
   * @param low the false branch
   * @param high the true branch
   * @return a canonical internal BDD node
   */
  public final JBddNode findOrCreate(JBddVariable var, JBddNode low, JBddNode high) {
    int index = HashFunction.hash(var.hashCode(), low.hashCode(), high.hashCode()) % this.tableSize;
    PhantomJBddNodeReference el = this.tableEntries[index];
    
    if (PROFILING) step();
    
    while (el != null) {
      JBddNode node = el.getNode();
      if (node.matches(var, low, high)) {
        if (PROFILING) hit();
        return node;
      }
      el = el.getNext();
      if (PROFILING) step();
    }

    if (PROFILING) miss();
    // didn't find it, create one
    synchronized(this) {
      el = this.nodePool.makeElement(var, low, high);
      el.setNext(this.tableEntries[index]);
      this.tableEntries[index] = el; // put it at the beginning of queue
    }

    return el.getNode();
  }

  /* Notifies a node is recycled. Removes the entry for the node.
   * The call chain of this method is from findOrCreate ->
   * PhantomNodePool.makeNode -> recycle ..., so it is already sync'ed.
   *
   * NOTE: the hash code of a node into this table is always made of
   *   its variable, low, and high. It is not the hashCode returned by the node.
   * Invariant: if a phantome reference is in the queue, it must has an
   *   entry in the unique table too.
   */
  protected void reclaim(PhantomJBddNodeReference toremove) {
    JBddNode node = toremove.getNode();
    int index = HashFunction.hash(node.variable.hashCode(), 
                                  node.low.hashCode(), 
                                  node.high.hashCode()) % this.tableSize;
    PhantomJBddNodeReference prev = null;
    PhantomJBddNodeReference el = this.tableEntries[index];
   
    while (el != toremove) {prev = el; el = el.getNext();}
    
    // assert el != null;

    if (prev != null) {
      prev.setNext(el.getNext());
    } else {
      this.tableEntries[index] = el.getNext();
    }
  }
}

/**
 * A phantom node pool preallocates a set of nodes, and keep a phantom reference on it
 * for recycling.
 */
class PhantomJBddNodePool {
  private final static boolean DEBUG = true;
  
  /* keep reusing phantom references for nodes to avoid allocating references whenever 
   * a node is allocated. However, freerefs and freenodes have to be synchronized.
   */
  private PhantomJBddNodeReference freerefs; // a list of free references to nodes.
  private JBddNode freenodes;      // keep free nodes strongly reachable.
  private ReferenceQueue refq;     // phantom references and their referents can be recycled

  private PhantomUniqueTable uniquetable; 

  private int poolsize;            // total pool size
  private int freesize;            // the number of free nodes;
  private float threshold;
  private float ratio;
  /* Creates a pool.
   * @param initsize, initial pool size
   * @param expanding_threshold, if the number of free nodes after GC is below the
   *                             threshold, expand the pool.
   * @param expanding_ratio, the expanding ratio
   */
  PhantomJBddNodePool(PhantomUniqueTable utable, 
		  int initsize, float expanding_threshold, float expanding_ratio) {
    this.uniquetable = utable;

    // initialize pool
    this.threshold = expanding_threshold;
    this.ratio = expanding_ratio;
    
    this.refq = new ReferenceQueue();

    expandPool(initsize);
  }

  private final void expandPool(int size) {
    PhantomJBddNodeReference   ref = this.freerefs;
    JBddNode         node = this.freenodes;
    for (int i=0; i<size; i++) {
      node = new JBddInternalNode(node);
      ref  = new PhantomJBddNodeReference(node, refq, ref);
    } 
    this.freenodes = node;
    this.freerefs  = ref;

    if (DEBUG) System.err.println("expand pool from "+this.poolsize+" to "+(this.poolsize+size));

    this.poolsize += size;
    this.freesize += size;
  }

  /* make a node from pool, if no free nodes, triggers gc and recycle nodes,
   * and expands pool if necessary.
   */
  PhantomJBddNodeReference makeElement(JBddVariable var, JBddNode low, JBddNode high) {
    if (this.freerefs == null) {
      // assert (this.freenodes == null);
      recycleAndExpand();
    }

    // assert (this.freerefs != null); // cannot be null, otherwise an OutOfMemoryError was thrown
    PhantomJBddNodeReference ref = this.freerefs;
    this.freerefs = ref.getNext();
    ref.clearNext();
    
    JBddNode node = this.freenodes;
    this.freenodes = node.getNext();
    node.clearNext();

    node.mutate(var, low, high);
    // assert (node == ref.getNode());
    
    this.freesize--;
    return ref;
  }

  // recycle node, fix uniquetable, and expand pool if necessary.
  private void recycleAndExpand() {
//    if (DEBUG) System.err.println("PhantomJBddNodePool.triggering GC...");
//    System.gc(); // call gc
    recycle(); // recycle nodes in reference queue
    if (DEBUG) System.err.println("recycled "+this.freesize+" out of "+this.poolsize+" nodes.");
    
    float liveratio = this.freesize/(float)this.poolsize;
    if (liveratio < this.threshold) {
      int expandsize = (int)(this.poolsize * this.ratio);
      expandPool(expandsize);
    }
  }

  private void recycle() {
    for (;;) {
      PhantomJBddNodeReference ref = (PhantomJBddNodeReference)this.refq.poll();
      if (ref == null) return;
      // notify unique table to remove a reclaimed node
      this.uniquetable.reclaim(ref);
      
      // ref is ready to be recycled
      ref.setNext(this.freerefs);
      this.freerefs = ref;
      
      // enqueue the node to be strongly reachable again
      JBddNode node = ref.getNode();
      node.reclaim();
      node.setNext(this.freenodes);
      this.freenodes = node;
      this.freesize ++;
    }
  }

  int size() {
    return this.poolsize;
  }
  
  int lives() {
    return this.poolsize - this.freesize;
  }
}


/** A phantom element is suitable for unique table. */
final class PhantomJBddNodeReference extends PhantomReference{
  protected static Field referent_field;
  static {
    try {
      referent_field = Reference.class.getDeclaredField("referent");
    } catch (Exception e) {
      e.printStackTrace();
      System.exit(1);
    }
  }
  
  PhantomJBddNodeReference next;       // next element
  PhantomJBddNodeReference(JBddNode node, ReferenceQueue q, PhantomJBddNodeReference next) {
    super(node, q);
    this.next = next;
  }
  
  JBddNode getNode() {
    try {
      referent_field.setAccessible(true);
      JBddNode node = (JBddNode)referent_field.get(this);
      referent_field.setAccessible(false);
      return node;
    } catch (IllegalAccessException iae) {
      throw new RuntimeException("cannot use reflection to implement node pool");
    }
  }

  PhantomJBddNodeReference getNext() {
    return this.next;
  }

  void clearNext() {
    this.next = null;
  }
  
  void setNext(PhantomJBddNodeReference next) {
    this.next = next;
  }
}
